mcsta

Benchmark
Model:coupon v.1 (DTMC)
Parameter(s)N = 9, DRAWS = 4, B = 5
Property:collect_all_bounded (prob-reach-reward-bounded)
Invocation (default)
mcsta/modest mcsta coupon.9-4.jani -E B=5 --props collect_all_bounded -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --reward-bounded-alg StateElimination
Execution
Walltime:79.00914859771729s
Return code:0
Note(s):The tool result '247219070403391/1250000000000000' is tagged as incorrect. The reference result is '1992983194384000/5559060566555523' (approx. 0.35851078982197204) which means a relative error of '0.4483422481623962' which is larger than the goal precision '1e-14'.
Relative Error:0.4483422481623962
Log
coupon.9-4.jani:model: info: coupon.9-4 is a DTMC model.
coupon.9-4.jani: info: Need 16 bytes per state.
coupon.9-4.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
coupon.9-4.jani: info: Explored 21077063 states for B=5.

Peak memory usage: 5447 MB
Analysis results for coupon.9-4.jani
Experiment B=5

+ State space exploration
  State size:  16 bytes
  States:      21077063
  Transitions: 21077063
  Branches:    24429223
  Rate:        1061496 states/s
  Time:        21.6 s

+ Property collect_all_bounded
  Probability: 0.1977752563227128
  Bounds:      [0.1977752563227128, 0.1977752563227128]
  CDF:         { (0, 0), ..., (2, 0), (3, 0.028620066090515834), (4, 0.13211546740874242), (5, 0.1977752563227128) }
  Time:        56.6 s

  + Essential states
    Iterations:       4
    Essential states: 3771692
    Transitions:      3771692
    Branches:         7123852
    Time:             3.4 s

  + State elimination
    States:      514
    Transitions: 514
    Branches:    113539
    Time:        53.1 s

  + Value iteration
    Time: 0.0 s

Exported results to file "/out.txt".
STDERR
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.